\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $R_{1}$, $R_{2}$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$), ${\it decodes}_{1}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{1}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),\+
\\[0ex]${\it decodes}_{2}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{2}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$), ${\it dec\_R}_{1}$:($i$:$C$$\rightarrow$$e$:E$\rightarrow$Dec($R_{1}$($i$,$e$))).
\-\\[0ex][$R_{1}$ ? ${\it decodes}_{1}$ : ${\it decodes}_{2}$] $\in$ $i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ ($R_{1}$($i$,$x$)) $\vee$ ($R_{2}$($i$,$x$))\} $\rightarrow$state@loc($e$)$\rightarrow$$T$
\end{tabbing}